es:ES, Qa, Rb, Sc:(EE), A, B, C:Type, Ia:AbsInterface(A), Ib:AbsInterface(B),
Ic:AbsInterface(C), f1:(E(Ia)B), f2:(BC), g1:(E(Ib)E(Ia)), g2:(E(Ic)E(Ib)).
(g1 glues Ia:Qa f1 Ib:Rb & g2 glues Ib:Rb e.f2(Ib(e)) Ic:Sc)
 g1 o g2 glues Ia:Qa f2 o f1 Ic:Sc 

latex

Definitions

s = t, t  T, ES, Type, , x:AB(x), AbsInterface(A), E(X), Q = f== P, f is Q-R-pre-preserving on P, Inj(A;B;f), <a, b>, x:A. B(x), x:A  B(x), b, left + right, x:A. B(x), e c e', P & Q, Q ==f== P, f(a), P  Q, E, {x:A| B(x)} , e  X, x.A(x), X(e), , f o g, a:A fp B(a), strong-subtype(A;B), x  dom(f), A c B, {I}, g glues Ia:Qa f Ib:Rb, EState(T), Id, , EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', constant_function(f;A;B), SWellFounded(R(x;y)), pred!(e;e'), x,y. t(x;y), Void, x:A.B(x), Top, S  T, suptype(S; T), first(e), A, pred(e), x. t(x), P  Q, P  Q, f(x)?z, let x,y = A in B(x;y), (x  l), False, True, case b of inl(x) => s(x) | inr(y) => t(y), tt, ff, t.1, inr x , inl x , {T}, T, SQType(T), s ~ t

Lemmas

subtype rel sum, strong-subtype-self, strong-subtype-set3, ext-eq weakening, subtype rel weakening, inject-composes, Q-R-pre-preserving-compose, squash wf, bfalse wf, btrue wf, false wf, true wf, subtype rel set, weak-antecedent-surjections-compose, es-interface-predicate wf, Q-R-glues wf, es-interface-val wf2, subtype rel function, es-E-interface-subtype rel, es-interface-subtype rel, es-interface wf, es-is-interface wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf, event system wf, weak-antecedent-function wf, weak-antecedent-surjection wf, Q-R-pre-preserving wf, inject wf, es-E-interface wf, assert wf, es-E wf, es-interface-val wf